A, B:Realizer.
R-Feasible(A)
 R-Feasible(B)
 A || B
 (R-size(A)  1)
 (R-size(B)  1)
 R-discrete(A) || R-discrete(B) 

latex

Definitions

t.1, f || g, T, p q, P  Q, P  Q, ff, tt, P  Q, True, if b then t else f fi , P & Q, {T}, SQType(T), x. t(x), Top, , t  T, R-discrete(R), P  Q, x:A. B(x), False, t.2, Unit, , A, R-discrete_compat(A;B), x(s), , Y, A || B, , Rinit-discrete(A), Reffect-discrete(A)

Lemmas

fpf-dom wf, R-discrete-base-dom, Rinit-discrete wf, Rinit-x wf, and functionality wrt iff, assert of band, bnot thru bor, band wf, assert of bor, bor wf, Rinit? wf, pi1 wf, pi2 wf, Reffect-discrete wf, Reffect-x wf, fpf-compatible-singles, R-discrete-base, Reffect? wf, fpf-compatible wf, fpf-compatible-self, R-base-domain wf, eq bd wf, not functionality wrt iff, assert-eq-id, R-loc wf, eq id wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, bool sq, bool cases, fpf-empty-compatible-right, top wf, fpf wf, fpf-trivial-subtype-top, R-discrete wf, id-deq wf, product-deq wf, Id wf, fpf-empty-compatible-left, Rnone-implies, Rnone? wf, not wf, bnot wf, assert wf, bool wf, Rplus-left wf, Rplus-right wf, R-size-decreases, Rplus? wf, es realizer wf, R-Feasible wf, R-compat wf, nat plus wf, R-size wf, le wf